ebab7d0da53c51438720d60c6e2e467c - /page/wikibook/entry.mu

<!DOCTYPE html>

<title>DPLL algorithm</title>

</head>

DPLL algorithm

</h1>

</header>

/* start https://en.wikipedia.org/ */

.mw-parser-output .infobox-subbox{padding:0;border:none;margin:-3px;width:auto;min-width:100%;font-size:100%;clear:none;float:none;background-color:transparent}.mw-parser-output .infobox-3cols-child{margin:auto}.mw-parser-output .infobox .navbar{font-size:100%}@media screen{html.skin-theme-clientpref-night .mw-parser-output .infobox-full-data:not(.notheme)>div:not(.notheme)[style]{background:#1f1f23!important;color:#f8f9fa}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .infobox-full-data:not(.notheme)>div:not(.notheme)[style]{background:#1f1f23!important;color:#f8f9fa}}@media(min-width:640px){body.skin--responsive .mw-parser-output .infobox-table{display:table!important}body.skin--responsive .mw-parser-output .infobox-table>caption{display:table-caption!important}body.skin--responsive .mw-parser-output .infobox-table>tbody{display:table-row-group}body.skin--responsive .mw-parser-output .infobox-table th,body.skin--responsive .mw-parser-output .infobox-table td{padding-left:inherit;padding-right:inherit}}

/* end https://en.wikipedia.org/ */

</style><table class="infobox"><caption class="infobox-title">DPLL</caption><tbody><tr><td colspan="2" class="infobox-image"><div class="infobox-caption">After 5 fruitless attempts (red), choosing the variable assignment a=1, b=1 leads, after unit propagation (bottom), to success (green): the top left <a href="Conjunctive_normal_form" title="Conjunctive normal form">CNF</a> formula is satisfiable.</div></td></tr><tr><th scope="row" class="infobox-label">Class</th><td class="infobox-data"><a href="Boolean_satisfiability_problem" title="Boolean satisfiability problem">Boolean satisfiability problem</a></td></tr><tr><th scope="row" class="infobox-label">Data structure</th><td class="infobox-data"><a href="Binary_tree" title="Binary tree">Binary tree</a></td></tr><tr><th scope="row" class="infobox-label"><a href="Best%2C_worst_and_average_case" title="Best, worst and average case">Worst-case</a> <a href="Time_complexity" title="Time complexity">performance</a></th><td class="infobox-data"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle O(2^{n})}">

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle O(2^{n})}</annotation>

</semantics>

</math><img src="./d4b1a4ff0bc4f81ebf79f28260c6fb54ee08ff8d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:5.964ex; height:2.843ex;" alt="{\displaystyle O(2^{n})}" loading="lazy"></td></tr><tr><th scope="row" class="infobox-label"><a href="Best%2C_worst_and_average_case" title="Best, worst and average case">Best-case</a> <a href="Time_complexity" title="Time complexity">performance</a></th><td class="infobox-data"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle O(1)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle O(1)}</annotation>

</semantics>

</math><img src="./e66384bc40452c5452f33563fe0e27e803b0cc21.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:4.745ex; height:2.843ex;" alt="{\displaystyle O(1)}" loading="lazy"> (constant)</td></tr><tr><th scope="row" class="infobox-label"><a href="Best%2C_worst_and_average_case" title="Best, worst and average case">Worst-case</a> <a href="Space_complexity" title="Space complexity">space complexity</a></th><td class="infobox-data"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle O(n)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle O(n)}</annotation>

</semantics>

</math><img src="./34109fe397fdcff370079185bfdb65826cb5565a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:4.977ex; height:2.843ex;" alt="{\displaystyle O(n)}" loading="lazy"> (basic algorithm)</td></tr></tbody></table>

In <a href="Logic" title="Logic">logic</a> and <a href="Computer_science" title="Computer science">computer science</a>, the Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a <a href="Completeness_(logic)" title="Completeness (logic)">complete</a>, <a href="Backtracking" title="Backtracking">backtracking</a>-based <a href="Search_algorithm" title="Search algorithm">search algorithm</a> for <a href="Boolean_satisfiability_problem" title="Boolean satisfiability problem">deciding the satisfiability</a> of <a href="Propositional_logic" title="Propositional logic">propositional logic formulae</a> in <a href="Conjunctive_normal_form" title="Conjunctive normal form">conjunctive normal form</a>, i.e. for solving the <a href="Boolean_satisfiability_problem" title="Boolean satisfiability problem">CNF-SAT</a> problem.

It was introduced in 1961 by <a href="Martin_Davis_(mathematician)" title="Martin Davis (mathematician)">Martin Davis</a>, <a href="George_Logemann" title="George Logemann">George Logemann</a> and <a href="Donald_W._Loveland" title="Donald W. Loveland">Donald W. Loveland</a> and is a refinement of the earlier <a href="Davis%E2%80%93Putnam_algorithm" title="Davis–Putnam algorithm">Davis–Putnam algorithm</a>, which is a <a href="Resolution_(logic)" title="Resolution (logic)">resolution</a>-based procedure developed by Davis and <a href="Hilary_Putnam" title="Hilary Putnam">Hilary Putnam</a> in 1960. Especially in older publications, the Davis–Logemann–Loveland algorithm is often referred to as the "Davis–Putnam method" or the "DP algorithm". Other common names that maintain the distinction are DLL and DPLL.

<div class="mw-heading mw-heading2"><h2 id="Implementations_and_applications">Implementations and applications</h2></div>

The <a href="Boolean_satisfiability_problem" title="Boolean satisfiability problem">SAT problem</a> is important both from theoretical and practical points of view. In <a href="Computational_complexity_theory" title="Computational complexity theory">complexity theory</a> it was the first problem proved to be <a href="NP-complete" class="mw-redirect" title="NP-complete">NP-complete</a>, and can appear in a broad variety of applications such as <a href="Model_checking" title="Model checking">model checking</a>, <a href="Automated_planning_and_scheduling" title="Automated planning and scheduling">automated planning and scheduling</a>, and <a href="Diagnosis_(artificial_intelligence)" title="Diagnosis (artificial intelligence)">diagnosis in artificial intelligence</a>.

As such, writing efficient <a href="SAT_solver" title="SAT solver">SAT solvers</a> has been a research topic for many years. <a href="GRASP_(SAT_solver)" title="GRASP (SAT solver)">GRASP</a> (1996-1999) was an early implementation using DPLL.<a href="#cite_note-DPLLT-1">[1]</a> In the international SAT competitions, implementations based around DPLL such as <a href="ZChaff" class="mw-redirect" title="ZChaff">zChaff</a><a href="#cite_note-2">[2]</a> and MiniSat<a href="#cite_note-3">[3]</a> were in the first places of the competitions in 2004 and 2005.<a href="#cite_note-comp-4">[4]</a>

Another application that often involves DPLL is <a href="Automated_theorem_proving" title="Automated theorem proving">automated theorem proving</a> or <a href="Satisfiability_modulo_theories" title="Satisfiability modulo theories">satisfiability modulo theories</a> (SMT), which is a SAT problem in which <a href="Propositional_variable" title="Propositional variable">propositional variables</a> are replaced with formulas of another <a href="Mathematical_theory" class="mw-redirect" title="Mathematical theory">mathematical theory</a>.

<div class="mw-heading mw-heading2"><h2 id="The_algorithm">The algorithm</h2></div>

The basic backtracking algorithm runs by choosing a literal, assigning a <a href="Truth_value" title="Truth value">truth value</a> to it, simplifying the formula and then recursively checking if the simplified formula is satisfiable; if this is the case, the original formula is satisfiable; otherwise, the same recursive check is done assuming the opposite truth value. This is known as the splitting rule, as it splits the problem into two simpler sub-problems. The simplification step essentially removes all clauses that become true under the assignment from the formula, and all literals that become false from the remaining clauses.

The DPLL algorithm enhances over the backtracking algorithm by the eager use of the following rules at each step:

<dl><dt><a href="Unit_propagation" title="Unit propagation">Unit propagation</a></dt>

<dd>If a clause is a unit clause, i.e. it contains only a single unassigned literal, this clause can only be satisfied by assigning the necessary value to make this literal true. Thus, no choice is necessary. Unit propagation consists in removing every clause containing a unit clause's literal and in discarding the complement of a unit clause's literal from every clause containing that complement. In practice, this often leads to deterministic cascades of units, thus avoiding a large part of the naive search space.</dd></dl>

<dl><dt>Pure literal elimination</dt>

<dd>If a <a href="Propositional_variable" title="Propositional variable">propositional variable</a> occurs with only one <a href="Polarity_(mathematical_logic)" class="mw-redirect" title="Polarity (mathematical logic)">polarity</a> in the formula, it is called pure. A pure literal can always be assigned in a way that makes all clauses containing it true. Thus, when it is assigned in such a way, these clauses do not constrain the search anymore, and can be deleted.</dd></dl>

Unsatisfiability of a given partial assignment is detected if one clause becomes empty, i.e. if all its variables have been assigned in a way that makes the corresponding literals false. Satisfiability of the formula is detected either when all variables are assigned without generating the empty clause, or, in modern implementations, if all clauses are satisfied. Unsatisfiability of the complete formula can only be detected after exhaustive search.

The DPLL algorithm can be summarized in the following pseudocode, where Φ is the <a href="Conjunctive_normal_form" title="Conjunctive normal form">CNF</a> formula:

<pre>Algorithm DPLL

Input: A set of clauses Φ.

Output: A truth value indicating whether Φ is satisfiable.

</pre>

<pre>function DPLL(Φ)

// unit propagation:

while there is a unit clause {l} in Φ do

Φ ← unit-propagate(l, Φ);

// pure literal elimination:

while there is a literal l that occurs pure in Φ do

Φ ← pure-literal-assign(l, Φ);

// stopping conditions:

if Φ is empty then

return true;

if Φ contains an empty clause then

return false;

// DPLL procedure:

l ← choose-literal(Φ);

return DPLL(Φ ∧ {l}) or DPLL(Φ ∧ {¬l});

</pre>

<ul><li>"←" denotes <a href="Assignment_(computer_science)" title="Assignment (computer science)">assignment</a>. For instance, "largest ← item" means that the value of largest changes to the value of item.</li>

<li>"return" terminates the algorithm and outputs the following value.</li></ul>

</div>

In this pseudocode, <code>unit-propagate(l, Φ)</code> and <code>pure-literal-assign(l, Φ)</code> are functions that return the result of applying unit propagation and the pure literal rule, respectively, to the literal <code>l</code> and the formula <code>Φ</code>. In other words, they replace every occurrence of <code>l</code> with "true" and every occurrence of <code>not l</code> with "false" in the formula <code>Φ</code>, and simplify the resulting formula. The <code>or</code> in the <code>return</code> statement is a <a href="Short-circuiting_operator" class="mw-redirect" title="Short-circuiting operator">short-circuiting operator</a>. <code>Φ ∧ {l}</code> denotes the simplified result of substituting "true" for <code>l</code> in <code>Φ</code>.

The algorithm terminates in one of two cases. Either the CNF formula <code>Φ</code> is empty, i.e., it contains no clause. Then it is satisfied by any assignment, as all its clauses are vacuously true. Otherwise, when the formula contains an empty clause, the clause is vacuously false because a disjunction requires at least one member that is true for the overall set to be true. In this case, the existence of such a clause implies that the formula (evaluated as a conjunction of all clauses) cannot evaluate to true and must be unsatisfiable.

The pseudocode DPLL function only returns whether the final assignment satisfies the formula or not. In a real implementation, the partial satisfying assignment typically is also returned on success; this can be derived by keeping track of branching literals and of the literal assignments made during unit propagation and pure literal elimination.

The Davis–Logemann–Loveland algorithm depends on the choice of branching literal, which is the literal considered in the backtracking step. As a result, this is not exactly an algorithm, but rather a family of algorithms, one for each possible way of choosing the branching literal. Efficiency is strongly affected by the choice of the branching literal: there exist instances for which the running time is constant or exponential depending on the choice of the branching literals. Such choice functions are also called <a href="Heuristic_function" class="mw-redirect" title="Heuristic function">heuristic functions</a> or branching heuristics.<a href="#cite_note-5">[5]</a>

<div class="mw-heading mw-heading3"><h3 id="Formalization">Formalization</h3></div>

The <a href="Sequent_calculus" title="Sequent calculus">sequent calculus</a>-similar notation can be used to formalize many rewriting algorithms, including DPLL. The following are the 5 rules a DPLL solver can apply in order to either find or fail to find a satisfying assignment, i.e. <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A=(l_{1},\neg l_{2},l_{3},...)}">

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle A=(l_{1},\neg l_{2},l_{3},...)}</annotation>

</semantics>

</math><img src="./9dc24831207ba1ec8318eb7bbfee210376331be4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:19.647ex; height:2.843ex;" alt="{\displaystyle A=(l_{1},\neg l_{2},l_{3},...)}" loading="lazy">.<a href="#cite_note-6">[6]</a><a href="#cite_note-7">[7]</a>

If a clause in the formula <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Phi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \Phi }</annotation>

</semantics>

</math><img src="./aed80a2011a3912b028ba32a52dfa57165455f24.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.678ex; height:2.176ex;" alt="{\displaystyle \Phi }" loading="lazy"> has exactly one unassigned literal <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle l}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle l}</annotation>

</semantics>

</math><img src="./829091f745070b9eb97a80244129025440a1cfac.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.693ex; height:2.176ex;" alt="{\displaystyle l}" loading="lazy"> in <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle A}</annotation>

</semantics>

</math><img src="./7daff47fa58cdfd29dc333def748ff5fa4c923e3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.743ex; height:2.176ex;" alt="{\displaystyle A}" loading="lazy">, with all other literals in the clause appearing negatively, extend <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle A}</annotation>

</semantics>

</math><img src="./7daff47fa58cdfd29dc333def748ff5fa4c923e3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.743ex; height:2.176ex;" alt="{\displaystyle A}" loading="lazy"> with <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle l}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle l}</annotation>

</semantics>

</math><img src="./829091f745070b9eb97a80244129025440a1cfac.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.693ex; height:2.176ex;" alt="{\displaystyle l}" loading="lazy">. This rule represents the idea a currently false clause with only one unset variable left forces that variable to be set in such a way as to make the entire clause true, otherwise the formula will not be satisfied.<math display="block" xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\frac {\begin{array}{c}\{l_{1},\dots ,l_{n},l\}\in \Phi \;\;\;\neg l_{1},\dots ,\neg l_{n}\in A\;\;\;\;\;l,\neg l\notin A\end{array}}{A:=A\;l}}{\text{ (Propagate)}}}">

<mfrac>

<mtr>

<mtd>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mtd>

</mtr>

</mtable>

<mrow>

</mrow>

</mfrac>

</mrow>

<mtext> (Propagate)</mtext>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\frac {\begin{array}{c}\{l_{1},\dots ,l_{n},l\}\in \Phi \;\;\;\neg l_{1},\dots ,\neg l_{n}\in A\;\;\;\;\;l,\neg l\notin A\end{array}}{A:=A\;l}}{\text{ (Propagate)}}}</annotation>

</semantics>

</math>If a literal <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle l}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle l}</annotation>

</semantics>

</math><img src="./829091f745070b9eb97a80244129025440a1cfac.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.693ex; height:2.176ex;" alt="{\displaystyle l}" loading="lazy"> appears in the formula <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Phi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \Phi }</annotation>

</semantics>

</math><img src="./aed80a2011a3912b028ba32a52dfa57165455f24.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.678ex; height:2.176ex;" alt="{\displaystyle \Phi }" loading="lazy"> but its negation <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \neg l}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \neg l}</annotation>

</semantics>

</math><img src="./3b619f4acdce5c7fdd09f0f1f254ac834125bc71.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.244ex; height:2.176ex;" alt="{\displaystyle \neg l}" loading="lazy"> does not, and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle l}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle l}</annotation>

</semantics>

</math><img src="./829091f745070b9eb97a80244129025440a1cfac.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.693ex; height:2.176ex;" alt="{\displaystyle l}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \neg l}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \neg l}</annotation>

</semantics>

</math><img src="./3b619f4acdce5c7fdd09f0f1f254ac834125bc71.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.244ex; height:2.176ex;" alt="{\displaystyle \neg l}" loading="lazy"> are not in <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle A}</annotation>

</semantics>

</math><img src="./7daff47fa58cdfd29dc333def748ff5fa4c923e3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.743ex; height:2.176ex;" alt="{\displaystyle A}" loading="lazy">, extend <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle A}</annotation>

</semantics>

</math><img src="./7daff47fa58cdfd29dc333def748ff5fa4c923e3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.743ex; height:2.176ex;" alt="{\displaystyle A}" loading="lazy"> with <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle l}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle l}</annotation>

</semantics>

</math><img src="./829091f745070b9eb97a80244129025440a1cfac.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.693ex; height:2.176ex;" alt="{\displaystyle l}" loading="lazy">. This rule represents the idea that if a variable appears only purely positively or purely negatively in a formula, all the instances can be set to true or false to make their corresponding clauses true.<math display="block" xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\frac {\begin{array}{c}l{\text{ literal of }}\Phi \;\;\;\neg l{\text{ not literal of }}\Phi \;\;\;\;\;l,\neg l\notin A\end{array}}{A:=A\;l}}{\text{ (Pure)}}}">

<mfrac>

<mtr>

<mtd>

<mtext> literal of </mtext>

</mrow>

<mtext> not literal of </mtext>

</mrow>

</mtd>

</mtr>

</mtable>

<mrow>

</mrow>

</mfrac>

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\frac {\begin{array}{c}l{\text{ literal of }}\Phi \;\;\;\neg l{\text{ not literal of }}\Phi \;\;\;\;\;l,\neg l\notin A\end{array}}{A:=A\;l}}{\text{ (Pure)}}}</annotation>

</semantics>

</math>If a literal <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle l}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle l}</annotation>

</semantics>

</math><img src="./829091f745070b9eb97a80244129025440a1cfac.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.693ex; height:2.176ex;" alt="{\displaystyle l}" loading="lazy"> is in the set of literals of <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Phi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \Phi }</annotation>

</semantics>

</math><img src="./aed80a2011a3912b028ba32a52dfa57165455f24.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.678ex; height:2.176ex;" alt="{\displaystyle \Phi }" loading="lazy"> and neither <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle l}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle l}</annotation>

</semantics>

</math><img src="./829091f745070b9eb97a80244129025440a1cfac.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.693ex; height:2.176ex;" alt="{\displaystyle l}" loading="lazy"> nor <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \neg l}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \neg l}</annotation>

</semantics>

</math><img src="./3b619f4acdce5c7fdd09f0f1f254ac834125bc71.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.244ex; height:2.176ex;" alt="{\displaystyle \neg l}" loading="lazy"> is in <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle A}</annotation>

</semantics>

</math><img src="./7daff47fa58cdfd29dc333def748ff5fa4c923e3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.743ex; height:2.176ex;" alt="{\displaystyle A}" loading="lazy">, then decide on the truth value of <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle l}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle l}</annotation>

</semantics>

</math><img src="./829091f745070b9eb97a80244129025440a1cfac.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.693ex; height:2.176ex;" alt="{\displaystyle l}" loading="lazy"> and extend <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle A}</annotation>

</semantics>

</math><img src="./7daff47fa58cdfd29dc333def748ff5fa4c923e3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.743ex; height:2.176ex;" alt="{\displaystyle A}" loading="lazy"> with the decision literal <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \bullet l}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \bullet l}</annotation>

</semantics>

</math><img src="./22e5f3f5f70e9b59ddd3c68c99e83e93641fbbee.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.856ex; height:2.176ex;" alt="{\displaystyle \bullet l}" loading="lazy">. This rule represents the idea that if you aren't forced to do an assignment, you must choose a variable to assign and make note which assignment was a choice so you can go back if the choice didn't result in a satisfying assignment.<math display="block" xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\frac {\begin{array}{c}l\in {\text{Lits}}(\Phi )\;\;\;l,\neg l\notin A\end{array}}{A:=A\;\bullet \;l}}{\text{ (Decide)}}}">

<mfrac>

<mtr>

<mtd>

</mrow>

</mtd>

</mtr>

</mtable>

<mrow>

</mrow>

</mfrac>

</mrow>

<mtext> (Decide)</mtext>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\frac {\begin{array}{c}l\in {\text{Lits}}(\Phi )\;\;\;l,\neg l\notin A\end{array}}{A:=A\;\bullet \;l}}{\text{ (Decide)}}}</annotation>

</semantics>

</math>If a clause <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \{l_{1},\dots ,l_{n}\}}">

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \{l_{1},\dots ,l_{n}\}}</annotation>

</semantics>

</math><img src="./f08833445d989b785e255ae63cbb671485c35170.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:11.162ex; height:2.843ex;" alt="{\displaystyle \{l_{1},\dots ,l_{n}\}}" loading="lazy"> is in <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Phi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \Phi }</annotation>

</semantics>

</math><img src="./aed80a2011a3912b028ba32a52dfa57165455f24.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.678ex; height:2.176ex;" alt="{\displaystyle \Phi }" loading="lazy">, and their negations <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \neg l_{1},\dots ,\neg l_{n}}">

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \neg l_{1},\dots ,\neg l_{n}}</annotation>

</semantics>

</math><img src="./7991411189478c0e619438c6cad3b8f5f1a66973.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:11.938ex; height:2.509ex;" alt="{\displaystyle \neg l_{1},\dots ,\neg l_{n}}" loading="lazy"> are in <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle A}</annotation>

</semantics>

</math><img src="./7daff47fa58cdfd29dc333def748ff5fa4c923e3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.743ex; height:2.176ex;" alt="{\displaystyle A}" loading="lazy">, and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle A}</annotation>

</semantics>

</math><img src="./7daff47fa58cdfd29dc333def748ff5fa4c923e3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.743ex; height:2.176ex;" alt="{\displaystyle A}" loading="lazy"> can be represented as <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A=A'\;\bullet \;l\;N}">

<msup>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle A=A'\;\bullet \;l\;N}</annotation>

</semantics>

</math><img src="./65f4cb7153d8ea7be228679c6c7b3ea47a5c15a4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:14.157ex; height:2.509ex;" alt="{\displaystyle A=A'\;\bullet \;l\;N}" loading="lazy"> where <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \bullet \notin N}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \bullet \notin N}</annotation>

</semantics>

</math><img src="./b82329d1326ad66c448b040c175c8e4859a76eae.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:6.067ex; height:2.676ex;" alt="{\displaystyle \bullet \notin N}" loading="lazy">, then backtrack by setting <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle A}</annotation>

</semantics>

</math><img src="./7daff47fa58cdfd29dc333def748ff5fa4c923e3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.743ex; height:2.176ex;" alt="{\displaystyle A}" loading="lazy"> to <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A'\;\neg l}">

<msup>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle A'\;\neg l}</annotation>

</semantics>

</math><img src="./95f8364cca5704e64ff75cfed2245aa04203fc19.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.317ex; height:2.509ex;" alt="{\displaystyle A'\;\neg l}" loading="lazy">. This rule represents the idea that if you reach a contradiction in trying to find a valid assignment, you need to go back to where you previously did a decision between two assignments and pick the other one.<math display="block" xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\frac {\begin{array}{c}\{l_{1},\dots ,l_{n}\}\in \Phi \;\;\;\neg l_{1},\dots ,\neg l_{n}\in A\;\;\;\;\;A=A'\;\bullet \;l\;N\;\;\;\;\;\bullet \notin N\end{array}}{A:=A'\;\neg l}}{\text{ (Backtrack)}}}">

<mfrac>

<mtr>

<mtd>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msup>

</msup>

</mtd>

</mtr>

</mtable>

<mrow>

<msup>

</msup>

</mrow>

</mfrac>

</mrow>

<mtext> (Backtrack)</mtext>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\frac {\begin{array}{c}\{l_{1},\dots ,l_{n}\}\in \Phi \;\;\;\neg l_{1},\dots ,\neg l_{n}\in A\;\;\;\;\;A=A'\;\bullet \;l\;N\;\;\;\;\;\bullet \notin N\end{array}}{A:=A'\;\neg l}}{\text{ (Backtrack)}}}</annotation>

</semantics>

</math>If a clause <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \{l_{1},\dots ,l_{n}\}}">

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \{l_{1},\dots ,l_{n}\}}</annotation>

</semantics>

</math><img src="./f08833445d989b785e255ae63cbb671485c35170.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:11.162ex; height:2.843ex;" alt="{\displaystyle \{l_{1},\dots ,l_{n}\}}" loading="lazy"> is in <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Phi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \Phi }</annotation>

</semantics>

</math><img src="./aed80a2011a3912b028ba32a52dfa57165455f24.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.678ex; height:2.176ex;" alt="{\displaystyle \Phi }" loading="lazy">, and their negations <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \neg l_{1},\dots ,\neg l_{n}}">

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \neg l_{1},\dots ,\neg l_{n}}</annotation>

</semantics>

</math><img src="./7991411189478c0e619438c6cad3b8f5f1a66973.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:11.938ex; height:2.509ex;" alt="{\displaystyle \neg l_{1},\dots ,\neg l_{n}}" loading="lazy"> are in <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle A}</annotation>

</semantics>

</math><img src="./7daff47fa58cdfd29dc333def748ff5fa4c923e3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.743ex; height:2.176ex;" alt="{\displaystyle A}" loading="lazy">, and there is no conflict marker <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \bullet }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \bullet }</annotation>

</semantics>

</math><img src="./3576c2406959ee194a6fc55c34b5ee9f6ffbb715.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: 0.125ex; margin-bottom: -0.297ex; width:1.162ex; height:1.509ex;" alt="{\displaystyle \bullet }" loading="lazy"> in <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle A}</annotation>

</semantics>

</math><img src="./7daff47fa58cdfd29dc333def748ff5fa4c923e3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.743ex; height:2.176ex;" alt="{\displaystyle A}" loading="lazy">, then the DPLL algorithm fails. This rule represents the idea that if you reach a contradiction but there wasn't anything you could have done differently on the way there, the formula is unsatisfiable.<math display="block" xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\frac {\begin{array}{c}\{l_{1},\dots ,l_{n}\}\in \Phi \;\;\;\neg l_{1},\dots ,\neg l_{n}\in A\;\;\;\;\;\bullet \notin A\end{array}}{\text{Fail}}}{\text{ (Fail)}}}">

<mfrac>

<mtr>

<mtd>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mtd>

</mtr>

</mtable>

</mfrac>

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\frac {\begin{array}{c}\{l_{1},\dots ,l_{n}\}\in \Phi \;\;\;\neg l_{1},\dots ,\neg l_{n}\in A\;\;\;\;\;\bullet \notin A\end{array}}{\text{Fail}}}{\text{ (Fail)}}}</annotation>

</semantics>

</math>

<div class="mw-heading mw-heading3"><h3 id="Visualization">Visualization</h3></div>

Davis, Logemann, Loveland (1961) had developed this algorithm.

Some properties of this original algorithm are:

<ul><li>It is based on search.</li>

<li>It is the basis for almost all modern SAT solvers.</li>

<li>It does not use learning or non-chronological backtracking (introduced in 1996).</li></ul>

An example with visualization of a DPLL algorithm having chronological backtracking:

<div class="gallerytext">All clauses making a CNF formula</div>

</li>

<div class="gallerytext">Pick a variable</div>

</li>

<div class="gallerytext">Make a decision, variable a = False (0), thus green clauses becomes True</div>

</li>

<div class="gallerytext">After making several decisions, we find an <a href="Implication_graph" title="Implication graph">implication graph</a> that leads to a conflict.</div>

</li>

<div class="gallerytext">Now backtrack to immediate level and by force assign opposite value to that variable</div>

</li>

<div class="gallerytext">But a forced decision still leads to another conflict</div>

</li>

<div class="gallerytext">Backtrack to previous level and make a forced decision</div>

</li>

<div class="gallerytext">Make a new decision, but it leads to a conflict</div>

</li>

<div class="gallerytext">Make a forced decision, but again it leads to a conflict</div>

</li>

<div class="gallerytext">Backtrack to previous level</div>

</li>

<div class="gallerytext">Continue in this way and the final implication graph</div>

</li>

</ul>

<div class="mw-heading mw-heading2"><h2 id="Related_algorithms">Related algorithms</h2></div>

Since 1986, (Reduced ordered) <a href="Binary_decision_diagram" title="Binary decision diagram">binary decision diagrams</a> have also been used for SAT solving.

In 1989-1990, Stålmarck's method for formula verification was presented and patented. It has found some use in industrial applications.<a href="#cite_note-8">[8]</a>

DPLL has been extended for <a href="Automated_theorem_proving" title="Automated theorem proving">automated theorem proving</a> for fragments of <a href="First-order_logic" title="First-order logic">first-order logic</a> by way of the <a href="DPLL(T)" title="DPLL(T)">DPLL(T)</a> algorithm.<a href="#cite_note-DPLLT-1">[1]</a>

In the 2010-2019 decade, work on improving the algorithm has found better policies for choosing the branching literals and new data structures to make the algorithm faster, especially the part on unit propagation. However, the main improvement has been a more powerful algorithm, <a href="Conflict-Driven_Clause_Learning" class="mw-redirect" title="Conflict-Driven Clause Learning">Conflict-Driven Clause Learning</a> (CDCL), which is similar to DPLL but after reaching a conflict "learns" the root causes (assignments to variables) of the conflict, and uses this information to perform non-chronological backtracking (aka <a href="Backjumping" title="Backjumping">backjumping</a>) in order to avoid reaching the same conflict again. Most state-of-the-art SAT solvers are based on the CDCL framework as of 2019.<a href="#cite_note-9">[9]</a>

<div class="mw-heading mw-heading2"><h2 id="Relation_to_other_notions">Relation to other notions</h2></div>

Runs of DPLL-based algorithms on unsatisfiable instances correspond to tree <a href="Resolution_(logic)" title="Resolution (logic)">resolution</a> refutation proofs.<a href="#cite_note-RossiBeek2006-10">[10]</a>

<ul><li><a href="Proof_complexity" title="Proof complexity">Proof complexity</a></li>

<li><a href="Herbrandization" title="Herbrandization">Herbrandization</a></li></ul>

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

General

/* start https://en.wikipedia.org/ */

.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}

/* end https://en.wikipedia.org/ */

</style><cite id="CITEREFDavisPutnam,_Hilary1960" class="citation journal cs1"><a href="Martin_Davis_(mathematician)" title="Martin Davis (mathematician)">Davis, Martin</a>; <a href="Hilary_Putnam" title="Hilary Putnam">Putnam, Hilary</a> (1960). <a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F321033.321034">"A Computing Procedure for Quantification Theory"</a>. <a href="Journal_of_the_ACM" title="Journal of the ACM">Journal of the ACM</a>. 7 (3): 201–215. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F321033.321034">10.1145/321033.321034</a>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:31888376">31888376</a>.</cite></li>

<li><cite id="CITEREFDavisLogemann,_GeorgeLoveland,_Donald1962" class="citation journal cs1">Davis, Martin; Logemann, George; Loveland, Donald (1962). <a rel="nofollow" class="external text" href="https://archive.org/details/machineprogramfo00davi">"A Machine Program for Theorem Proving"</a>. <a href="Communications_of_the_ACM" title="Communications of the ACM">Communications of the ACM</a>. 5 (7): 394–397. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F368273.368557">10.1145/368273.368557</a>. <a href="Hdl_(identifier)" class="mw-redirect" title="Hdl (identifier)">hdl</a>:<a rel="nofollow" class="external text" href="https://hdl.handle.net/2027%2Fmdp.39015095248095">2027/mdp.39015095248095</a>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:15866917">15866917</a>.</cite></li>

<li><cite id="CITEREFOuyang1998" class="citation journal cs1">Ouyang, Ming (1998). "How Good Are Branching Rules in DPLL?". Discrete Applied Mathematics. 89 (1–3): 281–286. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1016%2FS0166-218X%2898%2900045-6">10.1016/S0166-218X(98)00045-6</a>.</cite></li>

<li><cite id="CITEREFJohn_Harrison2009" class="citation book cs1">John Harrison (2009). Handbook of practical logic and automated reasoning. Cambridge University Press. pp. 79–90. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-0-521-89957-4</bdi>.</cite></li></ul>

Specific

/* start https://en.wikipedia.org/ */

.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}

/* end https://en.wikipedia.org/ */

</style><div class="reflist">

<cite id="CITEREFNieuwenhuisOliverasTinelli2004" class="citation cs2">Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesar (2004), <a rel="nofollow" class="external text" href="http://www.lsi.upc.edu/~roberto/papers/lpar04.pdf">"Abstract DPLL and Abstract DPLL Modulo Theories"</a> (PDF), Proceedings Int. Conf. on <a href="Logic_for_Programming%2C_Artificial_Intelligence%2C_and_Reasoning" class="mw-redirect" title="Logic for Programming, Artificial Intelligence, and Reasoning">Logic for Programming, Artificial Intelligence, and Reasoning</a>, LPAR 2004, pp. 36–50</cite>

</li>

<cite class="citation cs2"><a rel="nofollow" class="external text" href="http://www.princeton.edu/~chaff/zchaff.html">zChaff website</a></cite>

</li>

<cite class="citation web cs1"><a rel="nofollow" class="external text" href="http://minisat.se/">"Minisat website"</a>.</cite>

</li>

<cite class="citation cs2"><a rel="nofollow" class="external text" href="http://www.satcompetition.org/">The international SAT Competitions web page</a>, sat! live</cite>

</li>

<li id="cite_note-5"><a href="#cite_ref-5">^</a> <cite id="CITEREFMarques-Silva1999" class="citation book cs1">Marques-Silva, João P. (1999). "The Impact of Branching Heuristics in Propositional Satisfiability Algorithms". In Barahona, Pedro; Alferes, José J. (eds.). Progress in Artificial Intelligence: 9th Portuguese Conference on Artificial Intelligence, EPIA '99 Évora, Portugal, September 21–24, 1999 Proceedings. <a href="Lecture_Notes_in_Computer_Science" title="Lecture Notes in Computer Science">LNCS</a>. Vol. 1695. pp. 62–63. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F3-540-48159-1_5">10.1007/3-540-48159-1_5</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-3-540-66548-9</bdi>.</cite>

</li>

<li id="cite_note-6"><a href="#cite_ref-6">^</a> <cite id="CITEREFNieuwenhuisOliverasTinelli2006" class="citation journal cs1">Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare (2006-11-01). <a rel="nofollow" class="external text" href="https://dl.acm.org/doi/10.1145/1217856.1217859">"Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T)"</a>. J. ACM. 53 (6): 937–977. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F1217856.1217859">10.1145/1217856.1217859</a>. <a href="ISSN_(identifier)" class="mw-redirect" title="ISSN (identifier)">ISSN</a> <a rel="nofollow" class="external text" href="https://search.worldcat.org/issn/0004-5411">0004-5411</a>.</cite>

</li>

<li id="cite_note-7"><a href="#cite_ref-7">^</a> <cite id="CITEREFKrstićGoel2007" class="citation journal cs1">Krstić, Sava; Goel, Amit (2007). Konev, Boris; Wolter, Frank (eds.). <a rel="nofollow" class="external text" href="https://link.springer.com/chapter/10.1007/978-3-540-74621-8_1">"Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL"</a>. Frontiers of Combining Systems. Berlin, Heidelberg: Springer: 1–27. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-3-540-74621-8_1">10.1007/978-3-540-74621-8_1</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-3-540-74621-8</bdi>.</cite>

</li>

<li id="cite_note-8"><a href="#cite_ref-8">^</a> <cite id="CITEREFStålmarckSäflund1990" class="citation journal cs1">Stålmarck, G.; Säflund, M. (October 1990). "Modeling and Verifying Systems and Software in Propositional Logic". IFAC Proceedings Volumes. 23 (6): 31–36. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1016%2FS1474-6670%2817%2952173-4">10.1016/S1474-6670(17)52173-4</a>.</cite>

</li>

<li id="cite_note-9"><a href="#cite_ref-9">^</a> <cite id="CITEREFMöhleBiere2019" class="citation book cs1">Möhle, Sibylle; Biere, Armin (2019). "Backing Backtracking". <a rel="nofollow" class="external text" href="http://fmv.jku.at/papers/MoehleBiere-SAT19.pdf">Theory and Applications of Satisfiability Testing – SAT 2019</a> (PDF). Lecture Notes in Computer Science. Vol. 11628. pp. 250–266. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-3-030-24258-9_18">10.1007/978-3-030-24258-9_18</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-3-030-24257-2</bdi>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:195755607">195755607</a>.</cite>

</li>

<li id="cite_note-RossiBeek2006-10"><a href="#cite_ref-RossiBeek2006_10-0">^</a> <cite id="CITEREFVan_Beek2006" class="citation book cs1">Van Beek, Peter (2006). <a rel="nofollow" class="external text" href="https://books.google.com/books?id=Kjap9ZWcKOoC&pg=PA122">"Backtracking search algorithms"</a>. In Rossi, Francesca; Van Beek, Peter; Walsh, Toby (eds.). Handbook of constraint programming. Elsevier. p. 122. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-0-444-52726-4</bdi>.</cite>

</li>

</ol></div></div>

<div class="mw-heading mw-heading2"><h2 id="Further_reading">Further reading</h2></div>

<ul><li><cite id="CITEREFMalay_GanaiAarti_GuptaDr._Aarti_Gupta2007" class="citation book cs1">Malay Ganai; Aarti Gupta; Dr. Aarti Gupta (2007). SAT-based scalable formal verification solutions. Springer. pp. 23–32. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-0-387-69166-4</bdi>.</cite></li>

<li><cite id="CITEREFGomesKautzSabharwalSelman2008" class="citation book cs1">Gomes, Carla P.; Kautz, Henry; Sabharwal, Ashish; Selman, Bart (2008). "Satisfiability Solvers". In Van Harmelen, Frank; Lifschitz, Vladimir; Porter, Bruce (eds.). Handbook of knowledge representation. Foundations of Artificial Intelligence. Vol. 3. Elsevier. pp. 89–134. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1016%2FS1574-6526%2807%2903002-7">10.1016/S1574-6526(07)03002-7</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-0-444-52211-5</bdi>.</cite></li></ul></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2025-05-25" href="https://en.wikipedia.org/wiki/?title=DPLL_algorithm&oldid=1292217523">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>